Inductive InstrEval (st: State) : Instr -> State -> Prop :=
  | skip_eval :
      InstrEval st instr_skip st

  | assign_bool_eval : forall bid bexp b,
      BoolEval st bexp b -> InstrEval st (instr_assign_bool bid bexp) (Update st bid (bool_val b))

  | assign_int_eval : forall zid zexp z,
      ArithEval st zexp z -> InstrEval st (instr_assign_int zid zexp) (Update st zid (int_val z))

  | assign_byte_eval : forall bid bexp b,
      ByteEval st bexp (Some b) -> InstrEval st (instr_assign_byte bid bexp) (Update st bid (byte_val b))

  | assign_matrix_eval : forall mid (m n: Integer) (matr: Matrix Byte m n) (mexp : MatrixExp),
      MatrixEval st mexp matr -> InstrEval st (instr_assign_matrix mid mexp) (Update st mid (byte_matrix_val matr))

  | seq_eval : forall i1 i2 st' st'',
      InstrEval st i1 st' -> InstrEval st' i2 st'' -> InstrEval st (instr_seq i1 i2) st''

  | if_eval_true : forall bexp i1 i2 st',
      BoolEval st bexp TRUE -> InstrEval st i1 st' -> InstrEval st (instr_if bexp i1 i2) st'

  | if_eval_false : forall bexp i1 i2 st',
      BoolEval st bexp FALSE -> InstrEval st i2 st' -> InstrEval st (instr_if bexp i1 i2) st'

  | while_eval_true : forall bexp i st' st'',
      BoolEval st bexp TRUE -> InstrEval st i st' -> InstrEval st' (instr_while bexp i) st'' -> InstrEval st (instr_while bexp i) st''

  | while_eval_false : forall bexp i,
      BoolEval st bexp FALSE -> InstrEval st (instr_while bexp i) st

  | for_eval_end : forall i n instr,
      BoolEval st (bool_exp_ge (arith_exp_id i) n) TRUE -> InstrEval st (instr_for i n instr) st

  | for_eval_step : forall i x n instr st' st'',
      BoolEval st (bool_exp_lt (arith_exp_id i) n) TRUE -> InstrEval st instr st' -> 
      InstrEval st' (instr_for i n instr) st'' -> st' i = Some (int_val x) -> st'' i = Some (int_val (int_plus x ONE)) ->
      InstrEval st (instr_for i n instr) st''

  | matrix_set_eval : forall m n i j e1 e2 e mid (matr matr': Matrix Byte m n) b,
      MatrixEval st (matrix_exp_id mid) matr -> ArithEval st e1 i -> ArithEval st e2 j -> ByteEval st e (Some b) -> matrix_set matr i j b = Some matr' ->
      InstrEval st (instr_matrix_set mid e1 e2 e) (Update st mid (byte_matrix_val matr'))
.